Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use CBMC version 5.95.1 #108

Merged
merged 1 commit into from
Jul 31, 2024
Merged

Conversation

tautschnig
Copy link
Contributor

Description

The upcoming CBMC version 6 release includes changes that may affect existing proofs. This PR will make sure that coreMQTT-Agent PRs are not negatively impacted by this release. After releasing CBMC version 6 we will issue a follow-up PR that will return coreMQTT-Agent to using CBMC's latest release, and will include any changes to proofs that may be necessary to support the new version.

Test Steps

Tested in CI (no changes in behaviour at this point)

Checklist:

  • I have tested my changes. No regression in existing tests.
  • I have modified and/or added unit-tests to cover the code changes in this Pull Request.

Related Issue

n/a

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

The upcoming CBMC version 6 release includes changes that may affect
existing proofs. This PR will make sure that coreMQTT-Agent PRs are not
negatively impacted by this release. After releasing CBMC version 6 we
will issue a follow-up PR that will return coreMQTT-Agent to using
CBMC's latest release, and will include any changes to proofs that may
be necessary to support the new version.
@Skptak
Copy link
Member

Skptak commented Jun 6, 2024

It would probably make more sense to just increase the minimum version in the FreeRTOS/CI-CD-Github-Actions/set_up_cbmc_runner action/action.yml instead of creating a series of PRs across all the repos that consume this.

If you change all the users of the action to just use the default then only need to make the PR there to bump the version up. Saves you from having:

FreeRTOS/coreHTTP#181
FreeRTOS/coreJSON#164
#108
aws/ota-for-aws-iot-embedded-sdk#512
aws/SigV4-for-AWS-IoT-embedded-sdk#101
FreeRTOS/coreMQTT#289
FreeRTOS/corePKCS11#197
FreeRTOS/coreSNTP#94
aws/Device-Defender-for-AWS-IoT-embedded-sdk#85
aws/Device-Shadow-for-AWS-IoT-embedded-sdk#125
FreeRTOS/FreeRTOS#1226
FreeRTOS/FreeRTOS-Plus-TCP#1153
aws/Jobs-for-AWS-IoT-embedded-sdk#99
FreeRTOS/FreeRTOS-Cellular-Interface#174
aws/Fleet-Provisioning-for-AWS-IoT-embedded-sdk#44

Especially since the repos that are pulling in latest are already pulling 5.95.1, as seen in the coreJSON CBMC action, SigV4 CBMC action, and the coreMQTT CBMC action, for example.

@tautschnig
Copy link
Contributor Author

It would probably make more sense to just increase the minimum version in the FreeRTOS/CI-CD-Github-Actions/set_up_cbmc_runner action/action.yml instead of creating a series of PRs across all the repos that consume this.

Given the risk that changes in CBMC's back-end may adversely affect the performance of individual proofs (even when we are hoping it would generally just improve performance) I'd like to push back against this: on this one occasion of a major version bump I'd like to exercise extra care and only bump one repository at a time. Once we are happy with v6 across all FreeRTOS-related projects I'd agree that the right thing is to just leave it to the global config.

@AniruddhaKanhere AniruddhaKanhere merged commit afdd4d5 into FreeRTOS:main Jul 31, 2024
10 checks passed
@tautschnig tautschnig deleted the cbmc-5.95.1 branch August 23, 2024 13:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants